es:ES, i:Id, T:Type, ds:x:Id fp Type, P:(State(ds)TProp),
init:{f:x:Id fp ds(x)?Top| x:Id. x  dom(ds)  x  dom(f) }.
P holds in state init  e@i  Prop 

latex

Definitions	ES, t  T, Id, Type, x. t(x), x:A. B(x), a:A fp B(a), Prop, x:AB(x), State(ds), Top, IdDeq, x.A(x), f(x)?z, x  dom(f), b, P  Q, {x:A| B(x) }, loc(e), s = t, E, x:AB(x), x:A. B(x), f(a), P holds in state init  e@i, A, b, , P & Q, P  Q, Unit, left+right, f(x), Void, x:A. B(x), , False
Lemmas	it wf, fpf-ap wf, subtype rel self, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, not wf, es-E wf, es-loc wf, assert wf, fpf-dom wf, fpf-trivial-subtype-top, fpf-cap wf, id-deq wf, top wf, decl-state wf, fpf wf, Id wf, event system wf